/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.transform;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.Vector;

import salvo.jesus.graph.DirectedAcyclicGraph;
import salvo.jesus.graph.DirectedAcyclicGraphImpl;
import salvo.jesus.graph.Edge;
import salvo.jesus.graph.Vertex;
import alloy.ast.ASTDepthFirstVisitor;
import alloy.ast.Function;
import alloy.ast.InvocablePara;
import alloy.ast.Invocation;
import alloy.ast.InvocationExpr;
import alloy.ast.InvocationFormula;
import alloy.ast.Module;
import alloy.ast.ModuleInfo;
import alloy.ast.Predicate;
import alloy.ast.QualifiedName;
import alloy.util.Dbg;
import alloy.util.Msg;

/**
   Constructs an "invocation graph," in which nodes are invocables in the model
   and directed edges go from the invoker to invokee for any invocations
   appearing in the bodies of invocables.


   RECURSION IS NOT ALLOWED FOR NOW (Emina)

   Recursion is allowed, provided that one invocable in the cycle of invocations
   has all scalar arguments, at least one argument, and no polymorphism (for now).
   The function {@link #getSortedInvocables}
   returns a list of the invocables sorted such that no invocable contains an
   invocation of a invocable earlier in the list.  Certain invocables in the model
   will not appear in this list, since they need to be skolemized to handle recursion.
   This set of invocables can be obtained through the function {@link #getRecursiveInvocables}.
*/

public class ConstructInvocationGraphVisitor extends ASTDepthFirstVisitor {

    /** DAG representing invocation graph.  Note that to keep this graph as a DAG,
     certain functions which appear in recursive invocation cycles are removed.  */
    private DirectedAcyclicGraph _invocationDAG = new DirectedAcyclicGraphImpl();

    /**
       Set of invocables which need to be skolemized to handle recursion.
    */
    private Set _recursiveInvs = new HashSet();

    /**
     * mapping from {@link String} qualified invocable names to {@link Vertex}
     * vertices corresponding to the signatures
     */
    private Map _nameToVertex = new HashMap();

    /** current module scope */
    private ModuleInfo _curModuleInfo;

    /** current invocable vertex */
    private Vertex _curInvocableVertex;

    /**
     * set the current module scope and visit the
     * functions and predicates
     * @param module_ the Module
     */
    public void visit(Module module_) {
        _curModuleInfo = module_.getModuleInfo();
        module_.getFunctions().applyVisitor(this);
        module_.getPredicates().applyVisitor(this);
    }

    /**
     * set the current function vertex and then visit
     * the body of the function.
     */
    public void visit(Function function_) {
        visit((InvocablePara)function_);
    }

    /**
     * set the current predicate vertex and then visit
     * the body of the predicate.
     */
    public void visit(Predicate predicate_) {
        visit((InvocablePara)predicate_);
    }

    /**
     * set the current invocable vertex and then visit
     * the body of the invocable.
     */
    public void visit(InvocablePara invocable_) {
        _curInvocableVertex = getInvocableVertex(invocable_);
        invocable_.getFormula().applyVisitor(this);
    }

    /**
     * @return a list of the invocables in the specification, sorted
     * such that no invocable contains an invocation of an invocable appearing
     * later in the list.  A ConstructInvocationGraphVisitor must be
     * applied to the specification before this function is called.
     */
    public List getSortedInvocables() {
        Vector sort = _invocationDAG.reverseTopologicalSort();
        List invocables = new ArrayList();
        Iterator vertices = sort.iterator();
        while (vertices.hasNext()) {
            invocables.add(((Vertex)vertices.next()).getObject());
        }
        return invocables;
    }

    /**
       @return a set of invocables which, if skolemized, are sufficient
       to break all the cycles in the invocation graph
    */
    public Set getRecursiveInvocables() {
        return _recursiveInvs;
    }

    /**
     * add an edge from the current invocable to the invoked invocable.
     */
    private void  handleInvocation(Invocation invocation_) {
        // visit children
        super.visit(invocation_);
        // see if invoked invocable has already been removed
        InvocablePara invocable = invocation_.getInvocable();
        if (_recursiveInvs.contains(invocable)) {
            // don't re-add node for function, just return
            return;
        }
        Vertex invocableVertex = getInvocableVertex(invocable);
        // add the edge
        Edge addedEdge = _invocationDAG.addEdge(_curInvocableVertex,
                                                invocableVertex);
        // if edge is null, recursive invocations
        if (addedEdge == null) {
            // we won't handle recursion yet
            /**
                if (!_handleRecursion(_curInvocableVertex, invocableVertex)) {
                    Dbg.user(new Msg("recursive invocations with non-scalar args not currently supported",
                                     invocation_));
            }
            **/
             Dbg.user(new Msg("recursive invocations not currently supported",
                                     invocation_));
        }
    }

    /**
       @return <code>true</code> if the recursion caused by the invocation of invokedVertex_
       by curVertex_ can be handled by current techniques; <code>false</code> otherwise
    */
    /**
    private boolean _handleRecursion(Vertex curVertex_, Vertex invokedVertex_) {
        // first, try to skolemize the invoked vertex
        if (_addSkolemFun(invokedVertex_)) return true;
        // otherwise, try to find another function in the cycle to skolemize
        List path = _invocationDAG.getPath(invokedVertex_, curVertex_);
        Iterator pathIter = path.iterator();
        Dbg.chk(pathIter.next() == invokedVertex_);
        while (pathIter.hasNext()) {
            Vertex vertex = (Vertex)pathIter.next();
            if (_addSkolemFun(vertex)) {
                // need to add edge between curVertex_ and invokedVertex_
                // since now it doesn't cause cycle
                // only add edge if we're not skolemizing the invoking
                // function
                if (!(vertex == curVertex_)) {
                    Edge edge = _invocationDAG.addEdge(curVertex_, invokedVertex_);
                    Dbg.chk(edge);
                }
                return true;
            }
        }
        // if we reached here, tried all functions unsuccessfully
        return false;
    }
    **/

    /**
       try to mark the function represented by funVertex_ as one
       to be skolemized.  if the function is skolemizable, the vertex
       is removed from the invocation graph, and the function is
       appropriately marked.

       @return <code>true</code> if function represented by funVertex_
       can be skolemized; <code>false</code> otherwise
    */
    /**
    private boolean _addSkolemFun(Vertex funVertex_) {
        InvocablePara fun = (InvocablePara)funVertex_.getObject();
        // don't allow polymorphic functions (for now)
        if (!fun.getTypeParams().isLeaf()) return false;
        // check that all args have scalar multiplicities
        Decls argDecls = fun.getArgList().getArgDecls();
        Iterator declIter = argDecls.getDeclIter();
        // disallow case where there are no arguments
        if (!declIter.hasNext()) return false;
        while (declIter.hasNext()) {
            Decl curDecl = (Decl)declIter.next();
            // just check arity of type of multiplicity expression
            RelationType curType = curDecl.getExpr().getType();
            if (curType.numBasicTypes() > 1) return false;
            // don't support IntType yet
            if (!(curType.getBasicTypeAt(0) instanceof SigType)) return false;
        }
        // add function to list of recursive functions,
        // and remove from graph
        Dbg.chk(!_recursiveFuns.contains(fun));
        _recursiveFuns.add(fun);
        // i hope this works
        _invocationDAG.remove(funVertex_);
        return true;
    }
    **/

    public void visit(InvocationFormula invocationFormula_) {
        handleInvocation(invocationFormula_);
    }

    public void visit(InvocationExpr invocationExpr_) {
        handleInvocation(invocationExpr_);
    }

    /**
     * get the vertex for a function given its name, creating it
     * if necessary
     */
    private Vertex getInvocableVertex(QualifiedName invocableName_) {
        InvocablePara invocable = _curModuleInfo.getInvocable(invocableName_, "");
        Dbg.chk(invocable);
        return getInvocableVertex(invocable);
    }

    /**
     * return the existing vertex for an invocable if it has
     * been created, or a new vertex if it has not been created
     */
    private Vertex getInvocableVertex(InvocablePara invocable_) {
        // see if a node has already been created for the signature
        String invocableName = invocable_.getName().nodeString();
        Vertex invocableVertex = null;
        if (_nameToVertex.containsKey(invocableName)) {
            invocableVertex = (Vertex)_nameToVertex.get(invocableName);
        } else {
            // construct a new vertex and add it to the mapping
            // and graph
            invocableVertex = new Vertex(invocable_);
            _nameToVertex.put(invocableName, invocableVertex);
            _invocationDAG.add(invocableVertex);
        }
        return invocableVertex;
    }

}

